Exercise (Week 10)
Table of Contents
DUE: 20 May, 2018 23:55
Download the exercise tarball and extract it to a directory in your
home directory at CSE. This tarball contains a file, called Ex09.hs,
wherein you will do all of your programming.
To test your code, run the following shell commands to open a GHCi session:
$ 3141
newclass starting new subshell for class COMP3141...
$ cabal repl
Resolving dependencies...
Configuring Ex09-1.0...
Preprocessing executable 'Ex09' for Ex09-1.0..
GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Ex09 (Ex09.hs, interpreted)
Ok, one module loaded.
*Ex09> reflexivity SZero
...
Note that you will only need to submit Ex09.hs, so only make changes
to that file.
Download the exercise tarball and extract it to a directory on
your local machine. This tarball contains a file, called Ex09.hs,
wherein you will do all of your programming.
To test your code, run the following shell commands to open a GHCi session:
$ stack repl
Configuring GHCi with the following packages: Ex09
Using main module: 1. Package 'Ex09' component exe:Ex09 ...
GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Ex09 (Ex09.hs, interpreted)
Ok, one module loaded.
*Ex09> reflexivity SZero
...
Note that you will only need to submit Ex09.hs, so only make changes
to that file.
Download the Haskell for Mac project and unzip it somewhere on your
local machine. Open the project in Haskell for Mac, and begin
coding in Ex09.hs.
Note that you will only need to submit Ex09.hs, so only make changes
to that file.
1 Proofs and Types
Because of the Curry-Howard correspondence, if we write a total, terminating program in Haskell, it constitutes a proof of the proposition encoded by its type.
In this exercise, we'll define natural numbers, which we will use exclusively on the type level:
data Nat = Z | S Nat
We also define some singleton natural numbers type SNat to allow us to
examine a type-level Nat on the value level:
data SNat :: Nat -> * where SZero :: SNat Z SSucc :: SNat n -> SNat (S n)
Lastly, we will define a type LessEq a b that is inhabited only
when a is less than or equal to b:
data LessEq :: Nat -> Nat -> * where ZLEN :: LessEq Z n SLES :: LessEq n m -> LessEq (S n) (S m)
Each constructor of the LessEq type corresponds to an axiom about
the standard numerical ordering:
In this exercise, we'll prove some theorems about the \(\leq\) relation by writing total, terminating Haskell programs of the corresponding type.
1.1 Proving Reflexivity (Part 1, 3 Marks)
First we will prove reflexivity, that for all \(n\), \(n \leq n\). Normally we would prove this by doing an induction on \(n\) and proving the obligations that arise using the rules above. Inductive proofs correspond to (terminating) recursion via the Curry-Howard correspondence. So, to prove reflexivity in Haskell, we can write a function of the following type:
reflexivity :: SNat n -> LessEq n n
Implement this function, using recursion and by matching on the given number. If the function type-checks and returns a result for all inputs, it is a valid proof of reflexivity.
Any type-correct, total and terminating function will do – thus all our tests do is check that your function returns a result for any input.
1.2 Proving Transitivity (Part 2, 3 Marks)
Another theorem about natural number ordering we would like to prove is that of transitivity. Rather than do induction on a number, we must perform rule induction on the first inequality.
Once again, it suffices to implement a total, terminating function of the following type:
transitivity :: LessEq a b -> LessEq b c -> LessEq a c
1.3 Proving Antisymmetry (Part 3, 3 Marks)
We shall introduce a new type that is inhabited only if two indexed natural numbers are equal:
data Equal :: Nat -> Nat -> * where EqRefl :: Equal n n
Note that pattern matching on a value of type Equal a b will
inform the Haskell type checker that a and b are the same type.
Using this definition, prove antisymmetry of the \(\leq\) operator.
antisymmetry :: LessEq a b -> LessEq b a -> Equal a b antisymmetry _ _ = error "'antisymmetry' unimplemented"
Hint: use a case statement to pattern match on the result of the recursion,
introducing the type equality to the GHC type checker.
2 Submission instructions
$ give cs3141 Ex09 Ex09.hs
on a CSE terminal, or by using the give web interface. Your file must be named Ex09.hs (case-sensitive!).
A dry-run test will autotest your solution at submission time.